;; The first three lines of this file were inserted by DrRacket. They record metadata
;; about the language level of this file in a form that our tools can easily process.
#reader(lib "htdp-intermediate-lambda-reader.ss" "lang")((modname reachables-tues-1) (read-case-sensitive #t) (teachpacks ()) (htdp-settings #(#t constructor repeating-decimal #f #t none #f ())))
(require rackunit)
(require "extras.rkt")

;; Node = Int


;; Int -> SetOfInt
;; GIVEN: an integer
;; RETURNS: the list of its successors in the implicit graph.
;; For this graph, this is always a set (no repetitions)
(define (successors1 n)
  (if (<= n 0) 
      empty
      (local
        ((define n1 (quotient n 3)))
        (list n1 (+ n1 5)))))

(begin-for-test
  (check set-equal? (successors1 6) (list 2 7))
  (check set-equal? (successors1 2) (list 0 5))
  (check set-equal? (successors1 0) empty)
  (check set-equal? (successors1 5) (list 1 6))
  (check set-equal? (successors1 1) (list 0 5)))

;; reachable-n : SetOfNode Nat -> SetOfNode
;; GIVEN a set S of nodes and a NonNegInt n, 
;; RETURNS: the set of nodes
;; that are reachable from S in n or fewer steps
;; TERMINATION ARGUMENT: n is a halting measure
(define (reachable-n S n)
  (if (zero? n) 
      S
      (local
        ((define previous (reachable-n S (- n 1))))
        (set-union
         previous
         (all-successors previous)))))

(begin-for-test
  (check set-equal? (reachable (list 30) 0)
         (list 30))
  (check set-equal? (reachable (list 30) 1)
         (list 30 10 15))
  (check set-equal? (reachable (list 30) 2)
         (list 30 10 15 3 8 5)))



;; GIVEN: A node src, a set of nodes seen
;; WHERE: 
;;   (1) the number of nodes reachable from src 
;;       is finite AND
;;   (2) seen is (reachable-n {src} n) for some n.
;; RETURNS: the set of all nodes reachable from src.
;; STRATEGY: general recursion
;; TERMINATION ARGUMENT: The halting measure is: 
;; the number of nodes reachable from src that are NOT
;; in seen.
(define (reachable src seen)
  (local
    ((define new-nodes (all-successors seen)))
    (if (subset? new-nodes seen)
        seen
        (reachable src
                   (set-union new-nodes seen)))))

;; A termination argument consists of
;; -- a proposed halting measure
;; -- an argument as to why it really IS a halting measure.